\begin{tabbing}
$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $L$:($T$ List), $x$, $y$, $z$:$T$.
\\[0ex]$z$=$f$$\ast$($x$) via [$y$ / $L$]
\\[0ex]$\Leftarrow\!\Rightarrow$ \=\{$z$ = $y$\+
\\[0ex]\& ((0 $<$ $\parallel$$L$$\parallel$) $\Rightarrow$ ($y$ = $f$(hd($L$)) \& ($\neg$($y$ = hd($L$))) \& hd($L$)=$f$$\ast$($x$) via $L$))
\\[0ex]\& (($\neg$(0 $<$ $\parallel$$L$$\parallel$)) $\Rightarrow$ ($x$ = $y$))\}
\-
\end{tabbing}